(declare-sort S0 0)

(declare-sort S1 0)

(declare-sort S2 0)

(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const r3 Real)
(declare-const v17 Bool)
(assert v11)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const r4 Real)
(declare-const r5 Real)
(assert (<= 4641469.0 r4))
(assert (and v5 (< (+ (- (- r3 0.46843554 0.46843554)) (- r3 0.46843554 0.46843554) 4641469.0) 0.46843554) v12 v3 v10))
(check-sat)
